Nuprl Lemma : es-choose_wf
11,40
postcript
pdf
es
:event_system{i:l},
i
:Id.
es-choose(
es
;
i
)
b
:Id
es-state(
es
;
i
)
(?es-kindtype(
es
;
i
; locl(
b
)))
latex
Definitions
Unit
,
Type
,
t
T
,
f
(
a
)
,
left
+
right
,
x
:
A
B
(
x
)
,
Id
,
,
x
:
A
.
B
(
x
)
,
P
Q
,
es-T(
es
)
,
es-Choose(
es
)
,
es-V(
es
)
,
es-vartype(
es
;
i
;
x
)
,
act_locl{act_locl_compseq_tag_def:ObjectId}(
a
)
,
isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(
a
)
,
es-choose(
es
;
i
)
,
es-kindtype(
es
;
i
;
k
)
,
es-state(
es
;
i
)
,
x
:
A
B
(
x
)
,
event_system{i:l}
Lemmas
event
system
wf
,
Id
wf
,
subtype
rel
self
,
nat
wf
,
unit
wf
origin
es:event_system{i:l}, i:Id.
b:Id
es-state(es; i)(?es-kindtype(es; i; locl(b))) es:event_system{i:l}, i:Id.
b:Ides-state(es; i)(?es-kindtype(es; i; locl(b))) 
Q
B(x)